es:ES.
(e:E. state after e = Trans(loc(e))(kind(e),val(e),(state when e))  state@loc(e))
& (e:E.
& (islocal(kind(e))
& ( isl(Choose(loc(e))(act(kind(e)),(state when e)))
& ( & val(e) = outl(Choose(loc(e))(act(kind(e)),(state when e)))  valtype(e))
& (e:E.
& (isrcv(kind(e))
& ( (<lnk(kind(e)),tag(kind(e)),val(e)>  Send(loc(sender(e)))
& ( (<lnk(kind(e)),tag(kind(e)),val(e)>  (kind(sender(e))
& ( (<lnk(kind(e)),tag(kind(e)),val(e)>  ,val(sender(e))
& ( (<lnk(kind(e)),tag(kind(e)),val(e)>  ,(state when sender(e))))) 

latex

Definitions

x:AB(x), E, b, valtype(e), s = t, A & B, x:AB(x), P  Q, x:A. B(x), Msg, (x  l), P & Q, state@i, ES, t  T, state after e, <a,b>, Id, {T}, SQType(T), es_init(es), f(a), P  Q, P  Q, es-Trans(es), es_val(es), when-after(e;info;pred?;init;Trans;val), 2of(t), kind(e), x.A(x), let x = a in b(x), A, b, , Prop, es-pred?(es), first(e), Unit, left+right, (state when e), val(e), Trans(i), pred(e), loc(e), s ~ t, False, kind(e), isrcv(k), islocal(k), Type, if b t else f fi, val-axiom(E;V;M;info;pred?;init;Trans;Choose;Send;val), es_info(es), act(e), es-V(es), tag(e), lnk(e), es-M(es), es-Choose(es), acttype(e), rcvtype(e), isrcv(e), Choose(i), es-Send(es), sender(e), Send(i)

Lemmas

islocal wf, islocal-not-isrcv, isrcv wf, kind wf, es-loc-pred, eqtt to assert, iff transitivity, eqff to assert, assert of bnot, first wf, es-E wf, es-pred? wf, bool wf, bnot wf, not wf, assert wf, es-Trans wf, es-kind wf, es val wf, es-state-eta, es-state wf, es init wf, es-loc wf, Id sq, es-state-after wf, es-pred wf, event system wf